package tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism;

import java.util.HashSet;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.MergePair;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.MergeStrategy;
import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.syntax.atomicformula.SameIndividualAssertion;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class IdentificationBranchingPoint extends BranchingPoint {
	private int index;

	private Individual individual;

	private WorldConstraintSystem newWcs;

	private MergeStrategy mergeStrategy;

	private MergePair mergePair;

	public MergePair getMergePair() {
		return mergePair;
	}

	public void setMergePair(MergePair mergePair) {
		this.mergePair = mergePair;
	}

	public Individual getIndividual() {
		return individual;
	}

	public void setIndividual(Individual individual) {
		this.individual = individual;
	}

	public MergeStrategy getMergeStrategy() {
		return mergeStrategy;
	}

	public void setMergeStrategy(MergeStrategy mergeStrategy) {
		this.mergeStrategy = mergeStrategy;
	}

	@Override
	public boolean hasNext() {
		return index < 2;
	}

	@Override
	public WorldConstraintSystem next() throws UnsatisfiableException {
		if (index == 0) {
			newWcs = getWcs().copy();
			newWcs.setId(getWcs().getId() + 1);
			index++;
			ABox newABox = newWcs.getWorld(getWorld().getName()).getABox();
			getMergeStrategy().merge(getIndividual().getName(), newABox,
					getMergePair(), createDependencySet());
			newWcs.getData().getLogger().info(
					"WCS " + newWcs.getId() + " At most rule: Merged "
							+ getMergePair().getFrom() + " into "
							+ getMergePair().getInto());
		} else if (index == 1) {
			newWcs = getWcs();
			SameIndividualAssertion ia = new SameIndividualAssertion(
					getMergePair().getFrom(), getMergePair().getInto())
					.toggleNegated();
			getLastBranchDependencies().remove(getWcs());
			newWcs.getData().getDependencyManager().addAll(ia,
					getLastBranchDependencies());
			newWcs.getWorld(getWorld().getName()).add(ia);
			index++;
		}
		return newWcs;
	}

	private Set<WorldConstraintSystem> createDependencySet() {
		Set<WorldConstraintSystem> result = new HashSet<WorldConstraintSystem>();
		result.add(getWcs());
		return result;
	}

}
